Left Termination proof of /tmp/tmpNve5uH/snake.pl

Left Termination of the query pattern test_snake_in_3(g, g, g) w.r.t. the given Prolog program could not be shown:

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

Clauses:

test_snake(Pattern, C, R) :- ','(s2l(C, Cols), ','(s2l(R, Rows), snake(Pattern, Cols, Rows))).
s2l(0, []).
s2l(s(X), .(X1, Y)) :- s2l(X, Y).
snake(Pattern, Cols, Rows) :- ','(infinite_snake(Pattern, InfSnake, InfSnake), ','(produce_snake(Rows, Cols, InfSnake, Snake), coil_it(Snake, odd))).
infinite_snake([], S, S).
infinite_snake(.(A, R), .(A, T), S) :- infinite_snake(R, T, S).
produce_snake([], X, X1, []).
produce_snake(.(X, Rows), Cols, InfSnake, .(Part, Tail)) :- ','(part_of_snake(Cols, InfSnake, NewInfSnake, Part), produce_snake(Rows, Cols, NewInfSnake, Tail)).
part_of_snake([], RestSnake, RestSnake, []).
part_of_snake(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) :- part_of_snake(R, Rings, RestSnake, RestRings).
coil_it([], X).
coil_it(.(Line, Lines), odd) :- coil_it(Lines, even).
coil_it(.(Line, Lines), even) :- ','(reverse2(Line, Line1), coil_it(Lines, odd)).
reverse2(List, Reversed) :- reverse(List, [], Reversed).
reverse([], Reversed, Reversed).
reverse(.(Head, Tail), SoFar, Reversed) :- reverse(Tail, .(Head, SoFar), Reversed).

Queries:

test_snake(g,g,g).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

TEST_SNAKE_IN(Pattern, C, R) → U1¹(Pattern, C, R, s2l_in(C, Cols))
TEST_SNAKE_IN(Pattern, C, R) → S2L_IN(C, Cols)
S2L_IN(s(X), .(X1, Y)) → U4¹(X, X1, Y, s2l_in(X, Y))
S2L_IN(s(X), .(X1, Y)) → S2L_IN(X, Y)
U1¹(Pattern, C, R, s2l_out(C, Cols)) → U2¹(Pattern, C, R, Cols, s2l_in(R, Rows))
U1¹(Pattern, C, R, s2l_out(C, Cols)) → S2L_IN(R, Rows)
U2¹(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3¹(Pattern, C, R, snake_in(Pattern, Cols, Rows))
U2¹(Pattern, C, R, Cols, s2l_out(R, Rows)) → SNAKE_IN(Pattern, Cols, Rows)
SNAKE_IN(Pattern, Cols, Rows) → U5¹(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
SNAKE_IN(Pattern, Cols, Rows) → INFINITE_SNAKE_IN(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → U8¹(A, R, T, S, infinite_snake_in(R, T, S))
INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN(R, T, S)
U5¹(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6¹(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
U5¹(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → PART_OF_SNAKE_IN(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11¹(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN(R, Rings, RestSnake, RestRings)
U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10¹(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN(Rows, Cols, NewInfSnake, Tail)
U6¹(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7¹(Pattern, Cols, Rows, coil_it_in(Snake, odd))
U6¹(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN(Snake, odd)
COIL_IT_IN(.(Line, Lines), even) → U13¹(Line, Lines, reverse2_in(Line, Line1))
COIL_IT_IN(.(Line, Lines), even) → REVERSE2_IN(Line, Line1)
REVERSE2_IN(List, Reversed) → U15¹(List, Reversed, reverse_in(List, [], Reversed))
REVERSE2_IN(List, Reversed) → REVERSE_IN(List, [], Reversed)
REVERSE_IN(.(Head, Tail), SoFar, Reversed) → U16¹(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
REVERSE_IN(.(Head, Tail), SoFar, Reversed) → REVERSE_IN(Tail, .(Head, SoFar), Reversed)
U13¹(Line, Lines, reverse2_out(Line, Line1)) → U14¹(Line, Lines, coil_it_in(Lines, odd))
U13¹(Line, Lines, reverse2_out(Line, Line1)) → COIL_IT_IN(Lines, odd)
COIL_IT_IN(.(Line, Lines), odd) → U12¹(Line, Lines, coil_it_in(Lines, even))
COIL_IT_IN(.(Line, Lines), odd) → COIL_IT_IN(Lines, even)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in(x1, x2, x3) = test_snake_in(x1, x2, x3)
U1(x1, x2, x3, x4) = U1(x1, x3, x4)
s2l_in(x1, x2) = s2l_in(x1)
s(x1) = s(x1)
.(x1, x2) = .(x1, x2)
U4(x1, x2, x3, x4) = U4(x4)
0 = 0
[] = []
s2l_out(x1, x2) = s2l_out
U2(x1, x2, x3, x4, x5) = U2(x1, x5)
U3(x1, x2, x3, x4) = U3(x4)
snake_in(x1, x2, x3) = snake_in(x1)
U5(x1, x2, x3, x4) = U5(x4)
infinite_snake_in(x1, x2, x3) = infinite_snake_in(x1)
U8(x1, x2, x3, x4, x5) = U8(x5)
infinite_snake_out(x1, x2, x3) = infinite_snake_out
U6(x1, x2, x3, x4) = U6(x4)
produce_snake_in(x1, x2, x3, x4) = produce_snake_in
U9(x1, x2, x3, x4, x5, x6, x7) = U9(x7)
part_of_snake_in(x1, x2, x3, x4) = part_of_snake_in
U11(x1, x2, x3, x4, x5, x6, x7) = U11(x7)
part_of_snake_out(x1, x2, x3, x4) = part_of_snake_out
U10(x1, x2, x3, x4, x5, x6, x7) = U10(x7)
produce_snake_out(x1, x2, x3, x4) = produce_snake_out
U7(x1, x2, x3, x4) = U7(x4)
coil_it_in(x1, x2) = coil_it_in(x2)
odd = odd
even = even
U13(x1, x2, x3) = U13(x3)
reverse2_in(x1, x2) = reverse2_in
U15(x1, x2, x3) = U15(x3)
reverse_in(x1, x2, x3) = reverse_in
U16(x1, x2, x3, x4, x5) = U16(x5)
reverse_out(x1, x2, x3) = reverse_out
reverse2_out(x1, x2) = reverse2_out
U14(x1, x2, x3) = U14(x3)
U12(x1, x2, x3) = U12(x3)
coil_it_out(x1, x2) = coil_it_out
snake_out(x1, x2, x3) = snake_out
test_snake_out(x1, x2, x3) = test_snake_out
REVERSE_IN(x1, x2, x3) = REVERSE_IN
U11¹(x1, x2, x3, x4, x5, x6, x7) = U11¹(x7)
REVERSE2_IN(x1, x2) = REVERSE2_IN
U9¹(x1, x2, x3, x4, x5, x6, x7) = U9¹(x7)
SNAKE_IN(x1, x2, x3) = SNAKE_IN(x1)
COIL_IT_IN(x1, x2) = COIL_IT_IN(x2)
PRODUCE_SNAKE_IN(x1, x2, x3, x4) = PRODUCE_SNAKE_IN
U12¹(x1, x2, x3) = U12¹(x3)
U14¹(x1, x2, x3) = U14¹(x3)
U2¹(x1, x2, x3, x4, x5) = U2¹(x1, x5)
S2L_IN(x1, x2) = S2L_IN(x1)
U13¹(x1, x2, x3) = U13¹(x3)
U4¹(x1, x2, x3, x4) = U4¹(x4)
U16¹(x1, x2, x3, x4, x5) = U16¹(x5)
U7¹(x1, x2, x3, x4) = U7¹(x4)
TEST_SNAKE_IN(x1, x2, x3) = TEST_SNAKE_IN(x1, x2, x3)
U10¹(x1, x2, x3, x4, x5, x6, x7) = U10¹(x7)
U5¹(x1, x2, x3, x4) = U5¹(x4)
U3¹(x1, x2, x3, x4) = U3¹(x4)
PART_OF_SNAKE_IN(x1, x2, x3, x4) = PART_OF_SNAKE_IN
U8¹(x1, x2, x3, x4, x5) = U8¹(x5)
U6¹(x1, x2, x3, x4) = U6¹(x4)
U15¹(x1, x2, x3) = U15¹(x3)
INFINITE_SNAKE_IN(x1, x2, x3) = INFINITE_SNAKE_IN(x1)
U1¹(x1, x2, x3, x4) = U1¹(x1, x3, x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

TEST_SNAKE_IN(Pattern, C, R) → U1¹(Pattern, C, R, s2l_in(C, Cols))
TEST_SNAKE_IN(Pattern, C, R) → S2L_IN(C, Cols)
S2L_IN(s(X), .(X1, Y)) → U4¹(X, X1, Y, s2l_in(X, Y))
S2L_IN(s(X), .(X1, Y)) → S2L_IN(X, Y)
U1¹(Pattern, C, R, s2l_out(C, Cols)) → U2¹(Pattern, C, R, Cols, s2l_in(R, Rows))
U1¹(Pattern, C, R, s2l_out(C, Cols)) → S2L_IN(R, Rows)
U2¹(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3¹(Pattern, C, R, snake_in(Pattern, Cols, Rows))
U2¹(Pattern, C, R, Cols, s2l_out(R, Rows)) → SNAKE_IN(Pattern, Cols, Rows)
SNAKE_IN(Pattern, Cols, Rows) → U5¹(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
SNAKE_IN(Pattern, Cols, Rows) → INFINITE_SNAKE_IN(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → U8¹(A, R, T, S, infinite_snake_in(R, T, S))
INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN(R, T, S)
U5¹(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6¹(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
U5¹(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → PART_OF_SNAKE_IN(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11¹(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN(R, Rings, RestSnake, RestRings)
U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10¹(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN(Rows, Cols, NewInfSnake, Tail)
U6¹(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7¹(Pattern, Cols, Rows, coil_it_in(Snake, odd))
U6¹(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN(Snake, odd)
COIL_IT_IN(.(Line, Lines), even) → U13¹(Line, Lines, reverse2_in(Line, Line1))
COIL_IT_IN(.(Line, Lines), even) → REVERSE2_IN(Line, Line1)
REVERSE2_IN(List, Reversed) → U15¹(List, Reversed, reverse_in(List, [], Reversed))
REVERSE2_IN(List, Reversed) → REVERSE_IN(List, [], Reversed)
REVERSE_IN(.(Head, Tail), SoFar, Reversed) → U16¹(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
REVERSE_IN(.(Head, Tail), SoFar, Reversed) → REVERSE_IN(Tail, .(Head, SoFar), Reversed)
U13¹(Line, Lines, reverse2_out(Line, Line1)) → U14¹(Line, Lines, coil_it_in(Lines, odd))
U13¹(Line, Lines, reverse2_out(Line, Line1)) → COIL_IT_IN(Lines, odd)
COIL_IT_IN(.(Line, Lines), odd) → U12¹(Line, Lines, coil_it_in(Lines, even))
COIL_IT_IN(.(Line, Lines), odd) → COIL_IT_IN(Lines, even)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_IN(.(Head, Tail), SoFar, Reversed) → REVERSE_IN(Tail, .(Head, SoFar), Reversed)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_IN(.(Head, Tail), SoFar, Reversed) → REVERSE_IN(Tail, .(Head, SoFar), Reversed)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
REVERSE_IN(x1, x2, x3) = REVERSE_IN

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REVERSE_IN → REVERSE_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

REVERSE_IN → REVERSE_IN

The TRS R consists of the following rules:none

s = REVERSE_IN evaluates to t =REVERSE_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from REVERSE_IN to REVERSE_IN.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U13¹(Line, Lines, reverse2_out(Line, Line1)) → COIL_IT_IN(Lines, odd)
COIL_IT_IN(.(Line, Lines), odd) → COIL_IT_IN(Lines, even)
COIL_IT_IN(.(Line, Lines), even) → U13¹(Line, Lines, reverse2_in(Line, Line1))

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U13¹(Line, Lines, reverse2_out(Line, Line1)) → COIL_IT_IN(Lines, odd)
COIL_IT_IN(.(Line, Lines), odd) → COIL_IT_IN(Lines, even)
COIL_IT_IN(.(Line, Lines), even) → U13¹(Line, Lines, reverse2_in(Line, Line1))

The TRS R consists of the following rules:

reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
[] = []
odd = odd
even = even
reverse2_in(x1, x2) = reverse2_in
U15(x1, x2, x3) = U15(x3)
reverse_in(x1, x2, x3) = reverse_in
U16(x1, x2, x3, x4, x5) = U16(x5)
reverse_out(x1, x2, x3) = reverse_out
reverse2_out(x1, x2) = reverse2_out
COIL_IT_IN(x1, x2) = COIL_IT_IN(x2)
U13¹(x1, x2, x3) = U13¹(x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

COIL_IT_IN(odd) → COIL_IT_IN(even)
COIL_IT_IN(even) → U13¹(reverse2_in)
U13¹(reverse2_out) → COIL_IT_IN(odd)

The TRS R consists of the following rules:

reverse2_in → U15(reverse_in)
U15(reverse_out) → reverse2_out
reverse_in → U16(reverse_in)
reverse_in → reverse_out
U16(reverse_out) → reverse_out

The set Q consists of the following terms:

reverse2_in
U15(x0)
reverse_in
U16(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule COIL_IT_IN(even) → U13¹(reverse2_in) at position [0] we obtained the following new rules:

COIL_IT_IN(even) → U13¹(U15(reverse_in))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

COIL_IT_IN(odd) → COIL_IT_IN(even)
U13¹(reverse2_out) → COIL_IT_IN(odd)
COIL_IT_IN(even) → U13¹(U15(reverse_in))

The TRS R consists of the following rules:

reverse2_in → U15(reverse_in)
U15(reverse_out) → reverse2_out
reverse_in → U16(reverse_in)
reverse_in → reverse_out
U16(reverse_out) → reverse_out

The set Q consists of the following terms:

reverse2_in
U15(x0)
reverse_in
U16(x0)

We have to consider all (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

COIL_IT_IN(odd) → COIL_IT_IN(even)
U13¹(reverse2_out) → COIL_IT_IN(odd)
COIL_IT_IN(even) → U13¹(U15(reverse_in))

The TRS R consists of the following rules:

reverse_in → U16(reverse_in)
reverse_in → reverse_out
U15(reverse_out) → reverse2_out
U16(reverse_out) → reverse_out

The set Q consists of the following terms:

reverse2_in
U15(x0)
reverse_in
U16(x0)

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

reverse2_in

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

COIL_IT_IN(odd) → COIL_IT_IN(even)
U13¹(reverse2_out) → COIL_IT_IN(odd)
COIL_IT_IN(even) → U13¹(U15(reverse_in))

The TRS R consists of the following rules:

reverse_in → U16(reverse_in)
reverse_in → reverse_out
U15(reverse_out) → reverse2_out
U16(reverse_out) → reverse_out

The set Q consists of the following terms:

U15(x0)
reverse_in
U16(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

COIL_IT_IN(odd) → COIL_IT_IN(even)
U13¹(reverse2_out) → COIL_IT_IN(odd)
COIL_IT_IN(even) → U13¹(U15(reverse_in))

The TRS R consists of the following rules:

reverse_in → U16(reverse_in)
reverse_in → reverse_out
U15(reverse_out) → reverse2_out
U16(reverse_out) → reverse_out

s = U13¹(U15(reverse_in)) evaluates to t =U13¹(U15(reverse_in))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U13¹(U15(reverse_in)) → U13¹(U15(reverse_out))
with rule reverse_in → reverse_out at position [0,0] and matcher [ ]

U13¹(U15(reverse_out)) → U13¹(reverse2_out)
with rule U15(reverse_out) → reverse2_out at position [0] and matcher [ ]

U13¹(reverse2_out) → COIL_IT_IN(odd)
with rule U13¹(reverse2_out) → COIL_IT_IN(odd) at position [] and matcher [ ]

COIL_IT_IN(odd) → COIL_IT_IN(even)
with rule COIL_IT_IN(odd) → COIL_IT_IN(even) at position [] and matcher [ ]

COIL_IT_IN(even) → U13¹(U15(reverse_in))
with rule COIL_IT_IN(even) → U13¹(U15(reverse_in))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN(R, Rings, RestSnake, RestRings)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN(R, Rings, RestSnake, RestRings)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
PART_OF_SNAKE_IN(x1, x2, x3, x4) = PART_OF_SNAKE_IN

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN → PART_OF_SNAKE_IN

The TRS R consists of the following rules:none

s = PART_OF_SNAKE_IN evaluates to t =PART_OF_SNAKE_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from PART_OF_SNAKE_IN to PART_OF_SNAKE_IN.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
[] = []
part_of_snake_in(x1, x2, x3, x4) = part_of_snake_in
U11(x1, x2, x3, x4, x5, x6, x7) = U11(x7)
part_of_snake_out(x1, x2, x3, x4) = part_of_snake_out
U9¹(x1, x2, x3, x4, x5, x6, x7) = U9¹(x7)
PRODUCE_SNAKE_IN(x1, x2, x3, x4) = PRODUCE_SNAKE_IN

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U9¹(part_of_snake_out) → PRODUCE_SNAKE_IN
PRODUCE_SNAKE_IN → U9¹(part_of_snake_in)

The TRS R consists of the following rules:

part_of_snake_in → U11(part_of_snake_in)
part_of_snake_in → part_of_snake_out
U11(part_of_snake_out) → part_of_snake_out

The set Q consists of the following terms:

part_of_snake_in
U11(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule PRODUCE_SNAKE_IN → U9¹(part_of_snake_in) at position [0] we obtained the following new rules:

PRODUCE_SNAKE_IN → U9¹(part_of_snake_out)
PRODUCE_SNAKE_IN → U9¹(U11(part_of_snake_in))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U9¹(part_of_snake_out) → PRODUCE_SNAKE_IN
PRODUCE_SNAKE_IN → U9¹(U11(part_of_snake_in))
PRODUCE_SNAKE_IN → U9¹(part_of_snake_out)

The TRS R consists of the following rules:

part_of_snake_in → U11(part_of_snake_in)
part_of_snake_in → part_of_snake_out
U11(part_of_snake_out) → part_of_snake_out

The set Q consists of the following terms:

part_of_snake_in
U11(x0)

U9¹(part_of_snake_out) → PRODUCE_SNAKE_IN
PRODUCE_SNAKE_IN → U9¹(U11(part_of_snake_in))
PRODUCE_SNAKE_IN → U9¹(part_of_snake_out)

The TRS R consists of the following rules:

part_of_snake_in → U11(part_of_snake_in)
part_of_snake_in → part_of_snake_out
U11(part_of_snake_out) → part_of_snake_out

s = PRODUCE_SNAKE_IN evaluates to t =PRODUCE_SNAKE_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

PRODUCE_SNAKE_IN → U9¹(part_of_snake_out)
with rule PRODUCE_SNAKE_IN → U9¹(part_of_snake_out) at position [] and matcher [ ]

U9¹(part_of_snake_out) → PRODUCE_SNAKE_IN
with rule U9¹(part_of_snake_out) → PRODUCE_SNAKE_IN

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN(R, T, S)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN(R, T, S)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
INFINITE_SNAKE_IN(x1, x2, x3) = INFINITE_SNAKE_IN(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN(.(A, R)) → INFINITE_SNAKE_IN(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

INFINITE_SNAKE_IN(.(A, R)) → INFINITE_SNAKE_IN(R)
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN(s(X), .(X1, Y)) → S2L_IN(X, Y)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN(s(X), .(X1, Y)) → S2L_IN(X, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
.(x1, x2) = .(x1, x2)
S2L_IN(x1, x2) = S2L_IN(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2L_IN(s(X)) → S2L_IN(X)

From the DPs we obtained the following set of size-change graphs:

S2L_IN(s(X)) → S2L_IN(X)
The graph contains the following edges 1 > 1

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

TEST_SNAKE_IN(Pattern, C, R) → U1¹(Pattern, C, R, s2l_in(C, Cols))
TEST_SNAKE_IN(Pattern, C, R) → S2L_IN(C, Cols)
S2L_IN(s(X), .(X1, Y)) → U4¹(X, X1, Y, s2l_in(X, Y))
S2L_IN(s(X), .(X1, Y)) → S2L_IN(X, Y)
U1¹(Pattern, C, R, s2l_out(C, Cols)) → U2¹(Pattern, C, R, Cols, s2l_in(R, Rows))
U1¹(Pattern, C, R, s2l_out(C, Cols)) → S2L_IN(R, Rows)
U2¹(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3¹(Pattern, C, R, snake_in(Pattern, Cols, Rows))
U2¹(Pattern, C, R, Cols, s2l_out(R, Rows)) → SNAKE_IN(Pattern, Cols, Rows)
SNAKE_IN(Pattern, Cols, Rows) → U5¹(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
SNAKE_IN(Pattern, Cols, Rows) → INFINITE_SNAKE_IN(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → U8¹(A, R, T, S, infinite_snake_in(R, T, S))
INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN(R, T, S)
U5¹(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6¹(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
U5¹(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → PART_OF_SNAKE_IN(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11¹(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN(R, Rings, RestSnake, RestRings)
U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10¹(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN(Rows, Cols, NewInfSnake, Tail)
U6¹(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7¹(Pattern, Cols, Rows, coil_it_in(Snake, odd))
U6¹(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN(Snake, odd)
COIL_IT_IN(.(Line, Lines), even) → U13¹(Line, Lines, reverse2_in(Line, Line1))
COIL_IT_IN(.(Line, Lines), even) → REVERSE2_IN(Line, Line1)
REVERSE2_IN(List, Reversed) → U15¹(List, Reversed, reverse_in(List, [], Reversed))
REVERSE2_IN(List, Reversed) → REVERSE_IN(List, [], Reversed)
REVERSE_IN(.(Head, Tail), SoFar, Reversed) → U16¹(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
REVERSE_IN(.(Head, Tail), SoFar, Reversed) → REVERSE_IN(Tail, .(Head, SoFar), Reversed)
U13¹(Line, Lines, reverse2_out(Line, Line1)) → U14¹(Line, Lines, coil_it_in(Lines, odd))
U13¹(Line, Lines, reverse2_out(Line, Line1)) → COIL_IT_IN(Lines, odd)
COIL_IT_IN(.(Line, Lines), odd) → U12¹(Line, Lines, coil_it_in(Lines, even))
COIL_IT_IN(.(Line, Lines), odd) → COIL_IT_IN(Lines, even)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in(x1, x2, x3) = test_snake_in(x1, x2, x3)
U1(x1, x2, x3, x4) = U1(x1, x2, x3, x4)
s2l_in(x1, x2) = s2l_in(x1)
s(x1) = s(x1)
.(x1, x2) = .(x1, x2)
U4(x1, x2, x3, x4) = U4(x1, x4)
0 = 0
[] = []
s2l_out(x1, x2) = s2l_out(x1)
U2(x1, x2, x3, x4, x5) = U2(x1, x2, x3, x5)
U3(x1, x2, x3, x4) = U3(x1, x2, x3, x4)
snake_in(x1, x2, x3) = snake_in(x1)
U5(x1, x2, x3, x4) = U5(x1, x4)
infinite_snake_in(x1, x2, x3) = infinite_snake_in(x1)
U8(x1, x2, x3, x4, x5) = U8(x1, x2, x5)
infinite_snake_out(x1, x2, x3) = infinite_snake_out(x1)
U6(x1, x2, x3, x4) = U6(x1, x4)
produce_snake_in(x1, x2, x3, x4) = produce_snake_in
U9(x1, x2, x3, x4, x5, x6, x7) = U9(x7)
part_of_snake_in(x1, x2, x3, x4) = part_of_snake_in
U11(x1, x2, x3, x4, x5, x6, x7) = U11(x7)
part_of_snake_out(x1, x2, x3, x4) = part_of_snake_out
U10(x1, x2, x3, x4, x5, x6, x7) = U10(x7)
produce_snake_out(x1, x2, x3, x4) = produce_snake_out
U7(x1, x2, x3, x4) = U7(x1, x4)
coil_it_in(x1, x2) = coil_it_in(x2)
odd = odd
even = even
U13(x1, x2, x3) = U13(x3)
reverse2_in(x1, x2) = reverse2_in
U15(x1, x2, x3) = U15(x3)
reverse_in(x1, x2, x3) = reverse_in
U16(x1, x2, x3, x4, x5) = U16(x5)
reverse_out(x1, x2, x3) = reverse_out
reverse2_out(x1, x2) = reverse2_out
U14(x1, x2, x3) = U14(x3)
U12(x1, x2, x3) = U12(x3)
coil_it_out(x1, x2) = coil_it_out(x2)
snake_out(x1, x2, x3) = snake_out(x1)
test_snake_out(x1, x2, x3) = test_snake_out(x1, x2, x3)
REVERSE_IN(x1, x2, x3) = REVERSE_IN
U11¹(x1, x2, x3, x4, x5, x6, x7) = U11¹(x7)
REVERSE2_IN(x1, x2) = REVERSE2_IN
U9¹(x1, x2, x3, x4, x5, x6, x7) = U9¹(x7)
SNAKE_IN(x1, x2, x3) = SNAKE_IN(x1)
COIL_IT_IN(x1, x2) = COIL_IT_IN(x2)
PRODUCE_SNAKE_IN(x1, x2, x3, x4) = PRODUCE_SNAKE_IN
U12¹(x1, x2, x3) = U12¹(x3)
U14¹(x1, x2, x3) = U14¹(x3)
U2¹(x1, x2, x3, x4, x5) = U2¹(x1, x2, x3, x5)
S2L_IN(x1, x2) = S2L_IN(x1)
U13¹(x1, x2, x3) = U13¹(x3)
U4¹(x1, x2, x3, x4) = U4¹(x1, x4)
U16¹(x1, x2, x3, x4, x5) = U16¹(x5)
U7¹(x1, x2, x3, x4) = U7¹(x1, x4)
TEST_SNAKE_IN(x1, x2, x3) = TEST_SNAKE_IN(x1, x2, x3)
U10¹(x1, x2, x3, x4, x5, x6, x7) = U10¹(x7)
U5¹(x1, x2, x3, x4) = U5¹(x1, x4)
U3¹(x1, x2, x3, x4) = U3¹(x1, x2, x3, x4)
PART_OF_SNAKE_IN(x1, x2, x3, x4) = PART_OF_SNAKE_IN
U8¹(x1, x2, x3, x4, x5) = U8¹(x1, x2, x5)
U6¹(x1, x2, x3, x4) = U6¹(x1, x4)
U15¹(x1, x2, x3) = U15¹(x3)
INFINITE_SNAKE_IN(x1, x2, x3) = INFINITE_SNAKE_IN(x1)
U1¹(x1, x2, x3, x4) = U1¹(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

TEST_SNAKE_IN(Pattern, C, R) → U1¹(Pattern, C, R, s2l_in(C, Cols))
TEST_SNAKE_IN(Pattern, C, R) → S2L_IN(C, Cols)
S2L_IN(s(X), .(X1, Y)) → U4¹(X, X1, Y, s2l_in(X, Y))
S2L_IN(s(X), .(X1, Y)) → S2L_IN(X, Y)
U1¹(Pattern, C, R, s2l_out(C, Cols)) → U2¹(Pattern, C, R, Cols, s2l_in(R, Rows))
U1¹(Pattern, C, R, s2l_out(C, Cols)) → S2L_IN(R, Rows)
U2¹(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3¹(Pattern, C, R, snake_in(Pattern, Cols, Rows))
U2¹(Pattern, C, R, Cols, s2l_out(R, Rows)) → SNAKE_IN(Pattern, Cols, Rows)
SNAKE_IN(Pattern, Cols, Rows) → U5¹(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
SNAKE_IN(Pattern, Cols, Rows) → INFINITE_SNAKE_IN(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → U8¹(A, R, T, S, infinite_snake_in(R, T, S))
INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN(R, T, S)
U5¹(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6¹(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
U5¹(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → PART_OF_SNAKE_IN(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11¹(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN(R, Rings, RestSnake, RestRings)
U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10¹(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN(Rows, Cols, NewInfSnake, Tail)
U6¹(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7¹(Pattern, Cols, Rows, coil_it_in(Snake, odd))
U6¹(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN(Snake, odd)
COIL_IT_IN(.(Line, Lines), even) → U13¹(Line, Lines, reverse2_in(Line, Line1))
COIL_IT_IN(.(Line, Lines), even) → REVERSE2_IN(Line, Line1)
REVERSE2_IN(List, Reversed) → U15¹(List, Reversed, reverse_in(List, [], Reversed))
REVERSE2_IN(List, Reversed) → REVERSE_IN(List, [], Reversed)
REVERSE_IN(.(Head, Tail), SoFar, Reversed) → U16¹(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
REVERSE_IN(.(Head, Tail), SoFar, Reversed) → REVERSE_IN(Tail, .(Head, SoFar), Reversed)
U13¹(Line, Lines, reverse2_out(Line, Line1)) → U14¹(Line, Lines, coil_it_in(Lines, odd))
U13¹(Line, Lines, reverse2_out(Line, Line1)) → COIL_IT_IN(Lines, odd)
COIL_IT_IN(.(Line, Lines), odd) → U12¹(Line, Lines, coil_it_in(Lines, even))
COIL_IT_IN(.(Line, Lines), odd) → COIL_IT_IN(Lines, even)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_IN(.(Head, Tail), SoFar, Reversed) → REVERSE_IN(Tail, .(Head, SoFar), Reversed)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_IN(.(Head, Tail), SoFar, Reversed) → REVERSE_IN(Tail, .(Head, SoFar), Reversed)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

REVERSE_IN → REVERSE_IN

The TRS R consists of the following rules:none

s = REVERSE_IN evaluates to t =REVERSE_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from REVERSE_IN to REVERSE_IN.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U13¹(Line, Lines, reverse2_out(Line, Line1)) → COIL_IT_IN(Lines, odd)
COIL_IT_IN(.(Line, Lines), odd) → COIL_IT_IN(Lines, even)
COIL_IT_IN(.(Line, Lines), even) → U13¹(Line, Lines, reverse2_in(Line, Line1))

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U13¹(Line, Lines, reverse2_out(Line, Line1)) → COIL_IT_IN(Lines, odd)
COIL_IT_IN(.(Line, Lines), odd) → COIL_IT_IN(Lines, even)
COIL_IT_IN(.(Line, Lines), even) → U13¹(Line, Lines, reverse2_in(Line, Line1))

The TRS R consists of the following rules:

reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

COIL_IT_IN(odd) → COIL_IT_IN(even)
COIL_IT_IN(even) → U13¹(reverse2_in)
U13¹(reverse2_out) → COIL_IT_IN(odd)

The TRS R consists of the following rules:

reverse2_in → U15(reverse_in)
U15(reverse_out) → reverse2_out
reverse_in → U16(reverse_in)
reverse_in → reverse_out
U16(reverse_out) → reverse_out

The set Q consists of the following terms:

reverse2_in
U15(x0)
reverse_in
U16(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule COIL_IT_IN(even) → U13¹(reverse2_in) at position [0] we obtained the following new rules:

COIL_IT_IN(even) → U13¹(U15(reverse_in))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

COIL_IT_IN(odd) → COIL_IT_IN(even)
U13¹(reverse2_out) → COIL_IT_IN(odd)
COIL_IT_IN(even) → U13¹(U15(reverse_in))

The TRS R consists of the following rules:

reverse2_in → U15(reverse_in)
U15(reverse_out) → reverse2_out
reverse_in → U16(reverse_in)
reverse_in → reverse_out
U16(reverse_out) → reverse_out

The set Q consists of the following terms:

reverse2_in
U15(x0)
reverse_in
U16(x0)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

COIL_IT_IN(odd) → COIL_IT_IN(even)
U13¹(reverse2_out) → COIL_IT_IN(odd)
COIL_IT_IN(even) → U13¹(U15(reverse_in))

The TRS R consists of the following rules:

reverse_in → U16(reverse_in)
reverse_in → reverse_out
U15(reverse_out) → reverse2_out
U16(reverse_out) → reverse_out

The set Q consists of the following terms:

reverse2_in
U15(x0)
reverse_in
U16(x0)

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

reverse2_in

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

COIL_IT_IN(odd) → COIL_IT_IN(even)
U13¹(reverse2_out) → COIL_IT_IN(odd)
COIL_IT_IN(even) → U13¹(U15(reverse_in))

The TRS R consists of the following rules:

reverse_in → U16(reverse_in)
reverse_in → reverse_out
U15(reverse_out) → reverse2_out
U16(reverse_out) → reverse_out

The set Q consists of the following terms:

U15(x0)
reverse_in
U16(x0)

COIL_IT_IN(odd) → COIL_IT_IN(even)
U13¹(reverse2_out) → COIL_IT_IN(odd)
COIL_IT_IN(even) → U13¹(U15(reverse_in))

The TRS R consists of the following rules:

reverse_in → U16(reverse_in)
reverse_in → reverse_out
U15(reverse_out) → reverse2_out
U16(reverse_out) → reverse_out

s = U13¹(U15(reverse_in)) evaluates to t =U13¹(U15(reverse_in))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN(R, Rings, RestSnake, RestRings)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN(R, Rings, RestSnake, RestRings)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN → PART_OF_SNAKE_IN

The TRS R consists of the following rules:none

s = PART_OF_SNAKE_IN evaluates to t =PART_OF_SNAKE_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from PART_OF_SNAKE_IN to PART_OF_SNAKE_IN.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9¹(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U9¹(part_of_snake_out) → PRODUCE_SNAKE_IN
PRODUCE_SNAKE_IN → U9¹(part_of_snake_in)

The TRS R consists of the following rules:

part_of_snake_in → U11(part_of_snake_in)
part_of_snake_in → part_of_snake_out
U11(part_of_snake_out) → part_of_snake_out

The set Q consists of the following terms:

part_of_snake_in
U11(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule PRODUCE_SNAKE_IN → U9¹(part_of_snake_in) at position [0] we obtained the following new rules:

PRODUCE_SNAKE_IN → U9¹(part_of_snake_out)
PRODUCE_SNAKE_IN → U9¹(U11(part_of_snake_in))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U9¹(part_of_snake_out) → PRODUCE_SNAKE_IN
PRODUCE_SNAKE_IN → U9¹(U11(part_of_snake_in))
PRODUCE_SNAKE_IN → U9¹(part_of_snake_out)

The TRS R consists of the following rules:

part_of_snake_in → U11(part_of_snake_in)
part_of_snake_in → part_of_snake_out
U11(part_of_snake_out) → part_of_snake_out

The set Q consists of the following terms:

part_of_snake_in
U11(x0)

U9¹(part_of_snake_out) → PRODUCE_SNAKE_IN
PRODUCE_SNAKE_IN → U9¹(U11(part_of_snake_in))
PRODUCE_SNAKE_IN → U9¹(part_of_snake_out)

The TRS R consists of the following rules:

part_of_snake_in → U11(part_of_snake_in)
part_of_snake_in → part_of_snake_out
U11(part_of_snake_out) → part_of_snake_out

s = PRODUCE_SNAKE_IN evaluates to t =PRODUCE_SNAKE_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN(R, T, S)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN(R, T, S)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN(.(A, R)) → INFINITE_SNAKE_IN(R)

From the DPs we obtained the following set of size-change graphs:

INFINITE_SNAKE_IN(.(A, R)) → INFINITE_SNAKE_IN(R)
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN(s(X), .(X1, Y)) → S2L_IN(X, Y)

The TRS R consists of the following rules:

test_snake_in(Pattern, C, R) → U1(Pattern, C, R, s2l_in(C, Cols))
s2l_in(s(X), .(X1, Y)) → U4(X, X1, Y, s2l_in(X, Y))
s2l_in(0, []) → s2l_out(0, [])
U4(X, X1, Y, s2l_out(X, Y)) → s2l_out(s(X), .(X1, Y))
U1(Pattern, C, R, s2l_out(C, Cols)) → U2(Pattern, C, R, Cols, s2l_in(R, Rows))
U2(Pattern, C, R, Cols, s2l_out(R, Rows)) → U3(Pattern, C, R, snake_in(Pattern, Cols, Rows))
snake_in(Pattern, Cols, Rows) → U5(Pattern, Cols, Rows, infinite_snake_in(Pattern, InfSnake, InfSnake))
infinite_snake_in(.(A, R), .(A, T), S) → U8(A, R, T, S, infinite_snake_in(R, T, S))
infinite_snake_in([], S, S) → infinite_snake_out([], S, S)
U8(A, R, T, S, infinite_snake_out(R, T, S)) → infinite_snake_out(.(A, R), .(A, T), S)
U5(Pattern, Cols, Rows, infinite_snake_out(Pattern, InfSnake, InfSnake)) → U6(Pattern, Cols, Rows, produce_snake_in(Rows, Cols, InfSnake, Snake))
produce_snake_in(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in(R, Rings, RestSnake, RestRings))
part_of_snake_in([], RestSnake, RestSnake, []) → part_of_snake_out([], RestSnake, RestSnake, [])
U11(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out(R, Rings, RestSnake, RestRings)) → part_of_snake_out(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out(Cols, InfSnake, NewInfSnake, Part)) → U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in(Rows, Cols, NewInfSnake, Tail))
produce_snake_in([], X, X1, []) → produce_snake_out([], X, X1, [])
U10(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6(Pattern, Cols, Rows, produce_snake_out(Rows, Cols, InfSnake, Snake)) → U7(Pattern, Cols, Rows, coil_it_in(Snake, odd))
coil_it_in(.(Line, Lines), even) → U13(Line, Lines, reverse2_in(Line, Line1))
reverse2_in(List, Reversed) → U15(List, Reversed, reverse_in(List, [], Reversed))
reverse_in(.(Head, Tail), SoFar, Reversed) → U16(Head, Tail, SoFar, Reversed, reverse_in(Tail, .(Head, SoFar), Reversed))
reverse_in([], Reversed, Reversed) → reverse_out([], Reversed, Reversed)
U16(Head, Tail, SoFar, Reversed, reverse_out(Tail, .(Head, SoFar), Reversed)) → reverse_out(.(Head, Tail), SoFar, Reversed)
U15(List, Reversed, reverse_out(List, [], Reversed)) → reverse2_out(List, Reversed)
U13(Line, Lines, reverse2_out(Line, Line1)) → U14(Line, Lines, coil_it_in(Lines, odd))
coil_it_in(.(Line, Lines), odd) → U12(Line, Lines, coil_it_in(Lines, even))
coil_it_in([], X) → coil_it_out([], X)
U12(Line, Lines, coil_it_out(Lines, even)) → coil_it_out(.(Line, Lines), odd)
U14(Line, Lines, coil_it_out(Lines, odd)) → coil_it_out(.(Line, Lines), even)
U7(Pattern, Cols, Rows, coil_it_out(Snake, odd)) → snake_out(Pattern, Cols, Rows)
U3(Pattern, C, R, snake_out(Pattern, Cols, Rows)) → test_snake_out(Pattern, C, R)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN(s(X), .(X1, Y)) → S2L_IN(X, Y)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

S2L_IN(s(X)) → S2L_IN(X)

From the DPs we obtained the following set of size-change graphs:

S2L_IN(s(X)) → S2L_IN(X)
The graph contains the following edges 1 > 1